The present disclosure relates to enhanced case-splitting based property checking during circuit design formal verification. More particularly, the present disclosure relates to using a combination of case-splitting, property checking, and sequential equivalence checking to formally verify a circuit design model.
Circuit designers utilize a wide range of verification techniques to verify various stages of a circuit design as the circuit design migrates through different levels of design abstraction. Property checking is typically used to verify a circuit design model (e.g., register transfer language (RTL) model) against a circuit design specification. In particular, property checking verifies whether the circuit design model conforms to properties specified in the circuit design specification. As those skilled in the art can appreciate, a property is a set of assertions about design behavior of the circuit design under various sets of input conditions.
Sequential equivalence checking compares a validated model (e.g., a “reference model”) against a sequentially modified derivation of the validated model (e.g., a “model under verification”) to determine whether the model under verification is sequentially equivalent to the reference model. In general, sequential equivalence checking is more “expensive” in terms of time and processor resources compared with property checking. However, if the two models being compared have structural similarity, sequential equivalence checking may require less time and less resources than property checking.